Nuprl Definition : d-comp-partial-world 0,22

d-comp-partial-world(D;v;sched;dec;t)
== d-partial-world(D;CV(d-comp(D;v;sched;dec));t;i.if t=0 x.M(i).init(x)?v(i,x)
== d-partial-world(D;CV(d-comp(D;v;sched;dec));t;i.else 1of(CV(d-comp(D;v;sched;dec))
== d-partial-world(D;CV(d-comp(D;v;sched;dec));t;i.else 1of((t-1
== d-partial-world(D;CV(d-comp(D;v;sched;dec));t;i.else 1of(,i)) fi) 
latex



clarification:

d-comp-partial-world(D;v;sched;dec;t)
== d-partial-world(D;CV(d-comp(D;v;sched;dec));t;i.if t=0 x.d-m(Di).init(x)?v(i,x)
== d-partial-world(D;CV(d-comp(D;v;sched;dec));t;i.else 1of(CV(d-comp(D;v;sched;dec))
== d-partial-world(D;CV(d-comp(D;v;sched;dec));t;i.else 1of((t-1
== d-partial-world(D;CV(d-comp(D;v;sched;dec));t;i.else 1of(,i)) fi) 
latex


Definitionsd-partial-world(D;f;t';s), if b t else f fi, i=j, x.A(x), M.init(x)?v, M(i), 1of(t), f(a), CV(F), d-comp(D;v;sched;dec), n-m, #$n
FDL editor aliasesd-comp-partial-world

origin